signature VC_STRUCTS =
sig
  include ATOMS
end

signature VC =
sig
  include VC_STRUCTS
    
  datatype binop
    = Plus
    | Minus
    | Times
    | Divide
    | Modus
    | Band
    | Bor
    | Equ
    | NEqu
    | GT
    | GE
    | LT
    | LE 
    
  datatype mytype 
    = Int
    | Bool
    | Void
    | Struct of string
    | Pointer of mytype
    | Array of int * mytype

  datatype exp
    = Expvoid
    | IntNum of int
    | True
    | False
    | Null
    | Lval of lval
    | BinopExp of exp * binop * exp 
    | Not of exp  (*UnOp of unop * exp * pos *)
    (* below are added propositions... *)
    | Imply of exp * exp 
    (*| Iff of exp * exp * pos*) (* e1<=>e2 should be desugared to: e1=>e2 /\ e2=>e1 *)
    | Forall of string * mytype * exp  (* forall exp-- forall x:T.P*)
    | Exists of string * mytype * exp  (* exitst*)
    | Pi of lval list list  (*No Null No Dangling Pointer set *)
    | N of lval list (* Null pointer set*)
    | D of lval list  (* Dangling pointer set *)
    | Prev of lval (* previous value *)
    | LList of exp
    | Tree of exp
    | Pred of string * exp
    | Let of exp * exp * exp

  and lval
    = Var of string
    | Ptr of lval * lval    (*{ Sharp(T, lval) *)
    | Sharp of mytype              (*{ *)
    | Inarray of lval * exp
    | Instruct of lval * string
    | Instruct2 of lval * string * string
    | Upd of lval * exp * exp
    | Sel of lval * exp
  
  val compare : lval * lval -> order
  val twoLongIds : unit -> lval * lval
  val isPrefix : lval * lval -> bool
  val subst : lval * lval * lval -> lval
  val substDel : lval * lval -> lval
  val isStruct2 : lval -> bool
  val struct22id : lval -> lval
  
  val lval2str : lval -> string
  val ckE' : exp -> unit
  val ckE : exp -> unit
  val topOpt : exp -> exp
  val ppTop : (Id.t * exp) list * int -> unit
end
